package buffer

import chisel3._
import chiselFv.Formal

class Top(WIDTH : Int, PSIZE : Int, DEPTH : Int) extends Module with Formal{
  val depth = scala.math.pow(2,1.0 * PSIZE).toInt
  val io = IO(new Bundle{
//    val clk = Input(UInt(1.W))
//    val rst_n = Input(UInt(1.W))
    val in_wr = Input(Bool())
    val in_wdata = Input(UInt(WIDTH.W))
    val in_rd = Input(Bool())

    val out_rdata = Output(UInt(WIDTH.W))
    val out_empty = Output(Bool())
    val out_full = Output(Bool())

    val rnd_mark = Input(Bool())
  })

  val buffer = Mem(depth, UInt(WIDTH.W))
  val wrptr = RegInit(0.U(PSIZE.W))
  val rdptr = RegInit(0.U(PSIZE.W))
  val pdiff = (rdptr === (wrptr+1.U));//自然相等？引用相等？

  val out_rdata = RegInit(0.U(WIDTH.W))
  io.out_rdata := out_rdata

  val out_full = RegInit(false.B)
  io.out_full := out_full

  //buffer empty flag
  io.out_empty := (wrptr === rdptr) & ~out_full

  //buffer full flag
  when(pdiff && io.in_wr && !io.in_rd){
    out_full := true.B
  } .elsewhen(!io.in_wr && io.in_rd){
    out_full := false.B
  } .otherwise {
    out_full := out_full
  }

  //write ptr
  when(io.in_wr){
    when(wrptr < ((depth - 1).U)){
      wrptr := wrptr + 1.U
    } .otherwise{
      wrptr := 0.U(PSIZE.W)
    }
  } .otherwise{
    wrptr := wrptr
  }

  //read ptr
  when(io.in_rd){
    when(rdptr < ((depth - 1).U)){
      rdptr := rdptr + 1.U
    } .otherwise {
      rdptr := 0.U(PSIZE.W)
    }
  } .otherwise{
    rdptr := rdptr
  }

  //buffer
  when(io.in_wr) {
    buffer.write(wrptr, io.in_wdata)
  }

  //read data from buffer
  when(io.in_rd){
    out_rdata := buffer.read(rdptr)
  } .otherwise{
    out_rdata := out_rdata
  }

  //Assert Pass
  when(out_full){
    assume(!io.in_wr)
  }
  when(io.out_empty){
    assume(!io.in_rd)
  }

  val in_rd_ff1 = RegInit(false.B)
  val flag = RegInit(false.B)
  val rnd_mark = Wire(Bool())
  rnd_mark := io.rnd_mark

  val mark_vld = Wire(Bool())
  val check_vld = Wire(Bool())

  mark_vld := io.in_wr & rnd_mark
  check_vld := in_rd_ff1 & (out_rdata === 1.U(WIDTH.W))

  in_rd_ff1 := io.in_rd

  when(check_vld){
    flag := false.B
  } .elsewhen(mark_vld){
    flag := true.B
  }

  when(mark_vld){
    assume(io.in_wdata === 1.U(WIDTH.W))
  }
  when(!mark_vld && io.in_wr){
    assume(io.in_wdata === 0.U(WIDTH.W))
  }
  when(flag){
    assume(!mark_vld)
  }

  when(check_vld){
    assert(flag)
  }

  //Assert Fail
  // val check_vld_fail = Wire(Bool())
  // val flag_fail = RegInit(false.B)

  // check_vld_fail := in_rd_ff1 & (out_rdata + 2.U === 0.U)

  // when(check_vld_fail){
  //   flag_fail := false.B
  // } .elsewhen(mark_vld){
  //   flag_fail := true.B
  // }

  // when(flag_fail){
  //   assert(!mark_vld)
  // }
}